Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(D,t)	→ 1
2:		app(D,constant)	→ 0
3:		app(D,app(app(+,x),y))	→ app(app(+,app(D,x)),app(D,y))
4:		app(D,app(app(*,x),y))	→ app(app(+,app(app(,y),app(D,x))),app(app(,x),app(D,y)))
5:		app(D,app(app(-,x),y))	→ app(app(-,app(D,x)),app(D,y))

There are 15 dependency pairs:


6:		APP(D,app(app(+,x),y))	→ APP(app(+,app(D,x)),app(D,y))
7:		APP(D,app(app(+,x),y))	→ APP(+,app(D,x))
8:		APP(D,app(app(+,x),y))	→ APP(D,x)
9:		APP(D,app(app(+,x),y))	→ APP(D,y)
10:		APP(D,app(app(*,x),y))	→ APP(app(+,app(app(,y),app(D,x))),app(app(,x),app(D,y)))
11:		APP(D,app(app(*,x),y))	→ APP(+,app(app(*,y),app(D,x)))
12:		APP(D,app(app(*,x),y))	→ APP(app(*,y),app(D,x))
13:		APP(D,app(app(*,x),y))	→ APP(*,y)
14:		APP(D,app(app(*,x),y))	→ APP(D,x)
15:		APP(D,app(app(*,x),y))	→ APP(app(*,x),app(D,y))
16:		APP(D,app(app(*,x),y))	→ APP(D,y)
17:		APP(D,app(app(-,x),y))	→ APP(app(-,app(D,x)),app(D,y))
18:		APP(D,app(app(-,x),y))	→ APP(-,app(D,x))
19:		APP(D,app(app(-,x),y))	→ APP(D,x)
20:		APP(D,app(app(-,x),y))	→ APP(D,y)

The approximated dependency graph contains one SCC: {8,9,14,16,19,20}.

Consider the SCC {8,9,14,16,19,20}. There are no usable rules. By taking the AF π with π(APP) = 2 together with the lexicographic path order with empty precedence, the rules in {8,9,14,16,19,20} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.10 seconds) --- May 3, 2006